(FILECREATED "24-AUG-73 17:59:26" MOREFINDRULES)
(LISPXPRINT (QUOTE MOREFINDRULESVARS)
T)
[RPAQQ
MOREFINDRULESVARS
((VARS INEQUALITIES BAGARULES TOPRULES FAILINTODOWNRULES BAGEX
BAGEXCOMPLICATED INEQSTRIPSTRIP INEQIFTHENELSE BAGALOWERPLUS
INEQSTRIPTRAN INEQSTRIPBAG FIFTHENELSE DEDUCE LTPLUS ORSPLIT
ORSPLITMANY BAGEX1)
(P (DEFTYPE (QUOTE IFTHENELSE)
(QUOTE TUPLE))
[SETQ C1 (QUOTE (ASSERT (AND (SET]
[SETQ C2 (QUOTE (WHEN EXP (LTQ (SUBTRACT ←W ←X)
←Y)
INDICATOR MODELVALUE THEN
(PROG (DECLARE RTSIDE)
[SETQ ←RTSIDE
($TRYALL $PLUSRULES
(' (PLUS $Y $X]
(ASSERT (LTQ $W $RTSIDE)
WRT $VERICON]
[SETQ C3
(QUOTE (WHEN EXP (LT (SUBTRACT ←W ←X)
←Y)
INDICATOR MODELVALUE PUTS FALSE THEN
(PROG (DECLARE RTSIDE)
[SETQ
←RTSIDE
($TRYALL $PLUSRULES
(' (PLUS $Y $X
(MINUS 1]
(DENY (LTQ $W $RTSIDE)
WRT $VERICON]
[SETQ C4 (QUOTE (WHEN EXP (LTQ (PLUS (SUBTRACT ←W ←X)
←X)
←Y)
INDICATOR MODELVALUE THEN
(ASSERT (LTQ $W $Y)
WRT $VERICON]
[SETQ C5 (QUOTE (ASSERT (LTQ 1 M F N NN]
[SETQ C6 (QUOTE (ASSERT (LTQ M I]
[SETQ C7 (QUOTE (ASSERT (LTQ J N]
[SETQ C7.1 (QUOTE (ASSERT (LTQ (STRIP (BAGA A 1 (SUBTRACT
M 1)))
(STRIP (BAGA A M NN]
[SETQ C7.2 (QUOTE (ASSERT (LTQ (STRIP (BAGA A 1 N))
(STRIP (BAGA A (PLUS 1 N)
NN]
[SETQ C8 (QUOTE (ASSERT (LTQ (STRIP (BAGA A 1 (SUBTRACT I 1)))
R]
[SETQ C9 (QUOTE (ASSERT (LTQ R (STRIP (BAGA A (PLUS 1 J)
NN]
[SETQ C10 (QUOTE (ASSERT (LTQ (ACCESS A J)
R]
[SETQ C11 (QUOTE (ASSERT (LTQ R (ACCESS A I]
[SETQ C12 (QUOTE (ASSERT (LTQ I J]
[SETQ C13 (QUOTE (ASSERT (LT (SUBTRACT J 1)
(PLUS 1 I]
[SETQ C14 (QUOTE (ASSERT (LTQ F (SUBTRACT J 1]
[SETQQ C15 (GOAL $PROVE
(LTQ [STRIP (BAGA (EXCHANGE A I J)
1
((SUBTRACT J 1]
(STRIP (BAGA (EXCHANGE A I J)
(PLUS 1 (SUBTRACT J 1))
NN]
(FSETUP MOREFINDRULESVARS]
(RPAQQ INEQUALITIES
(TUPLE ANDSPLIT RELCHECK ORSPLIT ORSPLITMANY PROOFSIMP
INEQIFTHENELSE INEQSTRIPBAG INEQSTRIPSTRIP
INEQSTRIPTRAN GTQLTQ LTQMANY FSUBTRACT1 FSUBTRACT2
INEQTIMESDIVIDE EQINEQMONOTONE LTQPLUS PROOFLEIB
INEQLEIB))
(RPAQQ BAGARULES
(TUPLE BAGAPLUS BAGAEMPTY BAGAII ARGSIMP BACH BAGEX BAGEX1
BAGAMINUS BAGALOWERPLUS BAGEXCOMPLICATED))
(RPAQQ TOPRULES
(TUPLE HASSIMP FAILINTODOWNRULES PLUSOP TIMESOP MINUSOP
FIFTHENELSE BAGAOP SUBSTOP EXPZERO EXPEXP SUBPLUS
SUBNUM GCDEQ ACCH CONSDIFF DIFDIF DIFFCONS DIFFONE
MAXPLUS MAXONE BAGSTRIP ACCEX EQNUMB))
[RPAQQ FAILINTODOWNRULES (LAMBDA ←X
(IF (IN (STYPE $X)
(TUPLE TUPLE SET BAG))
THEN
(FAIL GOAL)
ELSE
(FAIL]
[RPAQQ BAGEX (LAMBDA (BAGA (EXCHANGE ←A ←I ←J)
←L ←M)
(PROG (DECLARE)
(GOAL $DEDUCE (LTQ $I $J))
(ATTEMPT
[GOAL $DEDUCE
(OR (AND (LTQ $L $I)
(LTQ $J $M))
(LT $J $L)
(LT $M $I)
(AND (LT $I $L)
(LT $M $J]
THEN
(RETURN (BAGA $A $L $M))
ELSE
(FAIL]
[RPAQQ
BAGEXCOMPLICATED
(LAMBDA
(BAGA (EXCHANGE ←A ←I ←J)
←L ←M)
(PROG (DECLARE)
(GOAL $DEDUCE (LTQ $I $J))
[ATTEMPT (GOAL $DEDUCE (AND (LTQ $L $I)
(LTQ $M $J)))
THEN
(RETURN (IFTHENELSE
(LT $M $I)
(BAGA $A $L $M)
(BAG (STRIP (BAGA $A $L (SUBTRACT $I 1)))
(ACCESS $A $J)
(STRIP (BAGA $A (PLUS 1 $I)
$M]
(ATTEMPT (GOAL $DEDUCE (AND (LTQ $J $M)
(LTQ $L $J)))
THEN
[RETURN (IFTHENELSE
(LTQ $L $I)
(BAGA $A $L $M)
(BAG (STRIP (BAGA $A $L (SUBTRACT $J 1)))
(ACCESS $A $I)
(STRIP (BAGA $A (PLUS 1 $J)
$M]
ELSE
(FAIL]
[RPAQQ INEQSTRIPSTRIP
(LAMBDA (←F (STRIP (BAGA ←A ←I ←J))
(STRIP (BAGA ←A ←K ←L)))
(PROG (DECLARE LOWER1 UPPER1 LOWER2 UPPER2 C D)
(ATTEMPT (EXISTS ($F (STRIP (BAGA $A ←LOWER1
←UPPER1))
←C))
[EXISTS ($F ←D
(STRIP (BAGA $A ←LOWER2
←UPPER2]
(GOAL $DEDUCE (AND (LTQ $LOWER1 $I)
(LTQ $J $UPPER1)
(LTQ $LOWER2 $K)
(LTQ $L $UPPER2)
(LTQ $C $D)))
ELSE
(FAIL]
[RPAQQ INEQIFTHENELSE (LAMBDA (←F ←←W1 (IFTHENELSE ←X ←Y ←Z)
←←W2)
(PROG (DECLARE VERICON)
(ATTEMPT (SETQ ←VERICON
(CONTEXT PUSH
LOCAL))
(ASSERT $X WRT $VERICON)
THEN
(GOAL $INEQUALITIES
($F $$W1 $Y $$W2)
WRT $VERICON))
(ATTEMPT (SETQ ←VERICON
(CONTEXT PUSH
LOCAL))
(DENY $X WRT $VERICON)
THEN
(GOAL $INEQUALITIES
($F $$W1 $Z $$W2)
WRT $VERICON)
ELSE
(RETURN (SUCCESS WITH
INEQIFTHENELSE]
[RPAQQ BAGALOWERPLUS
(LAMBDA (BAGA ←ARNAME ←L ←M)
(PROG (DECLARE F LOWER UPPER W)
(EXISTS (←F ←←V (STRIP (BAGA $ARNAME ←LOWER
←UPPER))
←←W))
(GOAL $DEDUCE (EQ $LOWER (PLUS 1 $L)))
(RETURN (BAG (ACCESS $ARNAME $L)
(STRIP (BAGA $ARNAME (PLUS 1 $L)
$M]
[RPAQQ INEQSTRIPTRAN
(LAMBDA (←F (STRIP (BAGA ←ARNAME ←L ←M))
←C)
(PROG (DECLARE LOWER UPPER D)
(EXISTS ($F (STRIP (BAGA $ARNAME ←LOWER ←UPPER))
←D))
(GOAL $DEDUCE (AND (LTQ $LOWER $L)
(LTQ $M $UPPER)
(LTQ $D $C]
[RPAQQ INEQSTRIPBAG (LAMBDA (←F ←←W (STRIP (BAG ←X ←←Y))
←←Z)
(GOAL $INEQUALITIES
(AND ($F $$W $X $$Z)
($F $$W (STRIP (BAG $$Y))
$$Z]
[RPAQQ FIFTHENELSE (LAMBDA (←F (IFTHENELSE ←W ←X ←Y))
(' (IFTHENELSE $W ($F $X)
($F $Y]
(RPAQQ DEDUCE
(TUPLE RELCHECK ANDSPLIT ORSPLIT ORSPLITMANY LTPLUS FSUBTRACT1
FSUBTRACT2 LTQPLUS NOTATOM CONSTCAR CONSTCDR))
(RPAQQ LTPLUS [LAMBDA (LT ←I (PLUS ←J ←K))
(GOAL $DEDUCE (AND (LTQ $I $J)
(LT 0 $K)))
BACKTRACK])
[RPAQQ ORSPLIT (LAMBDA (OR ←X ←Y)
(ATTEMPT (GOAL $GOALCLASS $X)
ELSE
(GOAL $GOALCLASS $Y]
[RPAQQ ORSPLITMANY (LAMBDA (OR ←X ←Y ←Z ←←W)
(ATTEMPT (GOAL $GOALCLASS $X)
ELSE
(GOAL $GOALCLASS
(OR $Y $Z $$W]
[RPAQQ BAGEX1
(LAMBDA
(BAGA (EXCHANGE ←A ←I ←J)
←L ←M)
(PROG (DECLARE)
(GOAL $DEDUCE (LTQ $I $J))
[ATTEMPT (GOAL $DEDUCE (AND (LT $I $L)
(LTQ $L $J)
(LTQ $J $M)))
THEN
(RETURN (BAG (STRIP (BAGA $A $L (SUBTRACT
$J 1)))
(ACCESS $A $I)
(STRIP (BAGA $A (PLUS 1 $J)
$M]
(ATTEMPT (GOAL $DEDUCE (AND (LT $M $J)
(LTQ $L $I)
(LTQ $I $M)))
THEN
[RETURN (BAG (STRIP (BAGA $A $L (SUBTRACT
$I 1)))
(ACCESS $A $J)
(STRIP (BAGA $A (PLUS 1 $I)
$M]
ELSE
(FAIL]
(DEFTYPE (QUOTE IFTHENELSE)
(QUOTE TUPLE))
[SETQ C1 (QUOTE (ASSERT (AND (SET]
[SETQ C2 (QUOTE (WHEN EXP (LTQ (SUBTRACT ←W ←X)
←Y)
INDICATOR MODELVALUE THEN
(PROG (DECLARE RTSIDE)
[SETQ ←RTSIDE ($TRYALL
$PLUSRULES
(' (PLUS $Y $X]
(ASSERT (LTQ $W $RTSIDE)
WRT $VERICON]
[SETQ C3 (QUOTE (WHEN EXP (LT (SUBTRACT ←W ←X)
←Y)
INDICATOR MODELVALUE PUTS FALSE THEN
(PROG (DECLARE RTSIDE)
[SETQ ←RTSIDE
($TRYALL
$PLUSRULES
(' (PLUS $Y $X (MINUS 1]
(DENY (LTQ $W $RTSIDE)
WRT $VERICON]
[SETQ C4 (QUOTE (WHEN EXP (LTQ (PLUS (SUBTRACT ←W ←X)
←X)
←Y)
INDICATOR MODELVALUE THEN (ASSERT (LTQ $W $Y)
WRT $VERICON]
[SETQ C5 (QUOTE (ASSERT (LTQ 1 M F N NN]
[SETQ C6 (QUOTE (ASSERT (LTQ M I]
[SETQ C7 (QUOTE (ASSERT (LTQ J N]
[SETQ C7.1 (QUOTE (ASSERT (LTQ (STRIP (BAGA A 1 (SUBTRACT M 1)))
(STRIP (BAGA A M NN]
[SETQ C7.2 (QUOTE (ASSERT (LTQ (STRIP (BAGA A 1 N))
(STRIP (BAGA A (PLUS 1 N)
NN]
[SETQ C8 (QUOTE (ASSERT (LTQ (STRIP (BAGA A 1 (SUBTRACT I 1)))
R]
[SETQ C9 (QUOTE (ASSERT (LTQ R (STRIP (BAGA A (PLUS 1 J)
NN]
[SETQ C10 (QUOTE (ASSERT (LTQ (ACCESS A J)
R]
[SETQ C11 (QUOTE (ASSERT (LTQ R (ACCESS A I]
[SETQ C12 (QUOTE (ASSERT (LTQ I J]
[SETQ C13 (QUOTE (ASSERT (LT (SUBTRACT J 1)
(PLUS 1 I]
[SETQ C14 (QUOTE (ASSERT (LTQ F (SUBTRACT J 1]
[SETQQ C15 (GOAL $PROVE (LTQ [STRIP (BAGA (EXCHANGE A I J)
1
((SUBTRACT J 1]
(STRIP (BAGA (EXCHANGE A I J)
(PLUS 1 (SUBTRACT J 1))
NN]
(FSETUP MOREFINDRULESVARS)
STOP